#include "luteco/lut.h"
#include "util/util.h"
#include "base/cktname.h"
#include "cktsat/msatsolver.h"
#include "util/usage.h"
#include <fstream>

using Minisat::l_True;
using std::vector;

extern bool gen_pattern( const StrashAIG & s , const StrashAIG & d , std::vector< pat_t > & pati , std::vector<bool> & );
extern void get_candidate( vector<unsigned> & cand , FPGA & design , 
      const StrashAIG & spec , const vector< pat_t > & pats , vector<pat_t> & gout , const vector<bool> & );
extern bool refine_candidate( vector<unsigned> & cand , const FPGA & design , 
      const vector< pat_t > & pati , const vector< pat_t > & pato );
extern unsigned synthesis_selection( Minisat::vec< Minisat::Lit>  & v ,const vector<unsigned> & cand ,const FPGA & design ,const StrashAIG & spec , const vector<pat_t> & pati , vector<pat_t> & pato , const vector<bool> & eqpo , unsigned pfcore , vector<pat_t> & learn );
extern void revise( FPGA & design , vector<unsigned> & cand , Minisat::vec< Minisat::Lit > & lutvalue );

///////////////////////////////////////
//      STATIC FUNCTION              //
///////////////////////////////////////
// use for blocking nonvalid assignment
static int index( const vector<string> & X , string x )
{ 
   for( unsigned i =0 ;i < X.size() ; ++ i) if( x == X[i] ) return i ; assert( false ); return -1; 
}
static void report_candidate( const vector<unsigned> & x, const vector<string> & y, unsigned base)
{
   cout << "candidate #" << x.size() << " ";
	for( unsigned i = 0 ; i < x.size() ; ++ i ) cout << x[i] << " "; cout << " name ";
   for( unsigned i = 0 ; i < x.size() ; ++ i )
      cout << y[ x[i] - base ] << " " ; 
   cout << endl;
}
static void getanswer( const vector<string> & names , unsigned base , const char * file , vector<unsigned> & ans){
   std::ifstream in( file );
   string str;
   unsigned num , seed , f1 , f2 , idx ;
   in >> str >> seed; assert( str == "seed" );
   in >> num >> std::hex ;
   for( unsigned i = 0; i < num ; ++ i ){
      in >> idx >> str >> f1 >> f2  ;
      ans.push_back( index( names , str ) + base );
   }
}
static void feedanswer( const vector<unsigned> & ans , vector<unsigned> & cand )
{
   unsigned hit = 0; 
   for( unsigned i = 0 ; i < ans.size() ; ++ i )
   {
      bool inside = false;
      
      for( unsigned j = 0 ; j < cand.size() ; ++ j ) 
         if( cand[j] == ans[i] ){ hit +=1 ; inside = true; break; }
      if( inside ) continue;

      cand.push_back( ans[i] );
   }
   cout <<"hit "<< hit <<"/"<< ans.size() <<"/"<< ( cand.size() - ans.size() + hit ) << endl;
}
static void hitanswer(  const vector<unsigned> & ans , const vector<unsigned> & cand )
{
   unsigned hit = 0;
   for( unsigned i = 0 ; i < ans.size() ; ++ i )
   {
      bool inside = false;
      
      for( unsigned j = 0 ; j < cand.size() ; ++ j ) 
         if( cand[j] == ans[i] ){ hit +=1 ; inside = true; break; }
      if( inside ) continue;
   }
   cout <<"hit "<< hit <<"/"<< ans.size() <<"/"<<  cand.size() << endl;
}
static bool eco_test( FPGA & design , const StrashAIG & spec , vector<unsigned> & ans , bool plot = false )
{
	unsigned ret;
	vector< pat_t > pats , gout , learn; 
	vector< bool > eqpo;
	vector< unsigned> cand;
	Minisat::vec< Minisat::Lit > lutvalue;
	
	// pattern generate 
	ret = gen_pattern( spec , *design.aig , pats , eqpo);  
	if( ret == false ){ cout << "res: equivalent " ; return true; }
	gout.resize( pats.size() );  
	for( unsigned i = 0 ; i < gout.size() ; ++ i ) gout[i].resize( design.po.size() );

	if( plot ) design.init_plot( pats.size() );

	get_candidate( cand , design , spec , pats , gout , eqpo );
	if( plot ) design.plot( "fpga.dot" , pats.size() , cand , ans );

	if( ans.size() ) feedanswer( ans , cand );	

	ret = refine_candidate( cand , design , pats , gout );
	if( ret == 0 ){ cout << "res: refine fail " << endl; return false ;}
	if( ans.size() ){ hitanswer( ans , cand ); cand = ans; }

  	lutvalue.clear() ; lutvalue.growTo( cand.size() << 4 );
	unsigned neqcnt = synthesis_selection( lutvalue , cand , design , spec , pats , gout , eqpo , Parameter::SYN_BY_SAT_CONFLICT , learn );
	if( neqcnt ){ cout << "res: synthesis lut fail" << endl; return false; }
	revise( design , cand , lutvalue );

   cout << "res: success" << endl;
	return true;
}
static bool eco( FPGA & design , const StrashAIG & spec )
{
	unsigned ret;
	vector< pat_t > pats , gout , learn;
	vector< bool > eqpo;
	vector< unsigned > cand;
	Minisat::vec< Minisat::Lit > lutvalue;

	while( 1 )
	{
		cout << endl;
		pats.clear() , gout.clear() , cand.clear() , lutvalue.clear();
		ret = gen_pattern( spec , *design.aig , pats , eqpo );
		if( ret == false )return true ; 
	
		gout.resize( pats.size() );
		for( unsigned i = 0 ; i < gout.size() ; ++i ) gout[i].resize( design.po.size() );
		cout << "pat size " << pats.size() << '\t'; cout.flush();
			
		get_candidate( cand , design , spec , pats , gout , eqpo );
		if( cand.size() == 0 ){
			continue;
		}
		cout << "cand size " << cand.size() << '\t'; cout.flush();

		ret = refine_candidate( cand , design , pats , gout );
		if( ret == 0 ){ 
			Parameter::change_pat( -1 );Parameter::change_cand1(1);Parameter::change();
			continue; 
		}
		cout << "cand size " << cand.size() << '\t'; cout.flush();
		
		lutvalue.clear(); lutvalue.growTo( cand.size() << 4 );
		clock_t init_clk = clock();
		for( unsigned i = 0 ; i < learn.size() ; ++i )pats.push_back( learn[i] );

		unsigned neqcnt = synthesis_selection( lutvalue , cand , design , spec , pats , gout , eqpo , Parameter::SYN_BY_SAT_CONFLICT , learn );
		cout << clock() - init_clk << "\t" ; cout.flush();
		
		if( Parameter::FIX_ALL == 0 || neqcnt == 0 )
			revise( design , cand , lutvalue );

		if( neqcnt == 0 ) return true;
		else
		{
			if( Parameter::FIX_ALL ==0 )	cout << "fix to " << neqcnt << '\t'; cout.flush();
			Parameter::change_pat(1);Parameter::change_cand1(1);	Parameter::change_cand2(1);Parameter::change();
			continue;
		}
	};

	return false;
}
//
//  create selection equivalence circuit
//
int main( int argc , const char ** argv )
{
   Usage usg;
   ArgAnalyzer arg( "eco <spec:aig> <lut:bench> <out:bench> [-plot] [-seed <unsigned:seed>] [-test] [-answer <string:file>] [-mode <int:mode>]" , argc , argv );
   
	if( arg["-seed"].setted )srand( atoi( arg["-seed"][0] ) );
	if( arg["-mode"].setted )Parameter::SYN_BY_SAT_CONFLICT = atoi( arg["-mode"][0] );

   FPGA 					design; 
   StrashAIG 			spec ; 
   CktName 			 	benchname , aigname ;
   vector<unsigned> 	ans;
	bool 					ret;

   // read 
   spec.read_aig( arg[0].c_str() , & aigname );
   design.read_bench( arg[1].c_str() , & benchname );
	if( spec._andFlag != design.andFlag-1 || spec._po.size() != design.po.size() ){ std::cerr << "Error: Spec and Design not match" << endl; exit(1);}

   design.init();
   design.report();
   if( arg["-answer"].setted ) getanswer( benchname.nodeName , design.andFlag , arg["-answer"][0] , ans);

	if( arg["-test"].setted )  
		ret = eco_test( design , spec , ans , arg["-plot"].setted );
	else 
		ret = eco( design , spec );

	if( ret == false )return -1;
   cout << "\nsucess" << endl;
	//design.write_bench( arg[2].c_str() , & aigname );

   usg.report();
	return 0;
}

